/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.generator.mcrl2;

import static nl.cwi.arne.generator.mcrl2.ArneMCRL2Translator.DELTA_TYPE;
import static nl.cwi.arne.generator.mcrl2.ArneMCRL2Translator.LEVEL_TYPE;
import nl.cwi.arne.Node;
import nl.cwi.arne.NodeActivation;
import nl.cwi.arne.mcrl2.Atom;
import nl.cwi.arne.mcrl2.BasicTerm;
import nl.cwi.arne.mcrl2.Comparator;
import nl.cwi.arne.mcrl2.Comparison;
import nl.cwi.arne.mcrl2.Equation;
import nl.cwi.arne.mcrl2.Function;
import nl.cwi.arne.mcrl2.FunctionCall;
import nl.cwi.arne.mcrl2.FunctionType;
import nl.cwi.arne.mcrl2.IfThenElse;
import nl.cwi.arne.mcrl2.Lambda;
import nl.cwi.arne.mcrl2.PrimitiveType;
import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.Term;
import nl.cwi.arne.mcrl2.TupleType;
import nl.cwi.arne.util.NodeActivationIndexConverter;

/**
 * Some static methods for creating functions needed
 * for the Arnce to mCRL2 translation.
 * @author Christian Krause
 */
public class ArneMCRL2FunctionFactory {

	/**
	 * Create the step function.
	 * @param specification Specification.
	 * @return The step function.
	 */
	public static Function createStepFunction(Specification specification) {
		
		// Function declaration:
		FunctionType type = new FunctionType(new TupleType(LEVEL_TYPE, LEVEL_TYPE), LEVEL_TYPE);
		Function function = new Function("step", type);
		specification.getFunctions().add(function);
		
		// Function definition:
		Lambda definition = new Lambda();
		Atom from = new Atom("from", LEVEL_TYPE);
		Atom to = new Atom("to", LEVEL_TYPE);
		definition.getArguments().add(from);
		definition.getArguments().add(to);
		
		Comparison greater = new Comparison(new BasicTerm(to), Comparator.GREATER, new BasicTerm(from));
		Comparison less = new Comparison(new BasicTerm(to), Comparator.LESS, new BasicTerm(from));
		Term one = new BasicTerm(1);
		Term minusone = new BasicTerm(-1);
		Term zero = new BasicTerm(0);
		
		definition.setBody(new IfThenElse(greater, one, new IfThenElse(less, minusone, zero)));
		specification.getEquations().add(new Equation(function, definition));
		return function;
		
	}

	/**
	 * Create the activation function for a given NodeActivation.
	 * @param activation Node activation.
	 * @param specification Specification.
	 * @return The mCRL2 activation function.
	 */
	public static Function createActivationFunction(NodeActivation activation, Specification specification) {
		
		Node node = activation.getNode();
		if (node.getIncoming().isEmpty()) {
			throw new IllegalArgumentException("Cannot create activation function for node " + node.getName() + " since it has no incoming edges");
		}
		int arcs = node.getIncoming().size();
		FunctionType type = new FunctionType();
		type.setDomain(new TupleType(PrimitiveType.BOOL, arcs));
		type.setCodomain(LEVEL_TYPE);
		Function function = new Function("act_" + node.getName(), type);
		specification.getFunctions().add(function);

		int permutations = NodeActivationIndexConverter.getIndexCount(arcs);
		for (int index=0; index<permutations; index++) {
			boolean[] resources = NodeActivationIndexConverter.getResources(index,arcs);
			FunctionCall left = new FunctionCall(function);
			for (int i=0; i<arcs; i++) {
				left.getArguments().add(new BasicTerm(resources[i]));
			}
			Term right = new BasicTerm(activation.getTargetLevel(resources));
			specification.getEquations().add(new Equation(left,right));
		}
		return function;
		
	}
	
	/**
	 * Create the change function for a given node.
	 * @param node Node.
	 * @param activation mCRL2 activation function for that node.
	 * @param step Step function.
	 * @return The change function.
	 */
	public static Function createChangeFunction(Node node, Function activation, Function step, Specification specification) {
		
		// Function declaration and definition:
		Lambda definition = new Lambda();
		NetworkArguments args = new NetworkArguments(node.getNetwork(), definition.getArguments(), LEVEL_TYPE, DELTA_TYPE);
		
		FunctionType type = new FunctionType(args.type(), LEVEL_TYPE);
		Function function = new Function("chg_" + node.getName(), type);
		specification.getFunctions().add(function);
		
		Term body;
		if (activation!=null) {
			FunctionCall activationCall = new FunctionCall(activation);
			activationCall.getArguments().addAll(ArneMCRL2ConstraintFactory.createNodeConstraint(node, args));
			body = new FunctionCall(step, new BasicTerm(args.level(node)), activationCall);
		} else {
			body = new BasicTerm(args.level(node));
		}
		definition.setBody(body);
		specification.getEquations().add(new Equation(new FunctionCall(function), definition));

		return function;
		
	}

}
